\begin{tabbing}
$\forall$\=$k$:Knd, $l$:IdLnk, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$a$:Knd fp$\rightarrow$ Type,\+
\\[0ex]$f$:(${\it tg}$:Id$\times$(State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;$k$)$\rightarrow$(${\it da}$(rcv($l$,${\it tg}$))?Void List))) List.
\-\\[0ex]$\forall$$x$$\in$dom(${\it ds}$). $A$=${\it ds}$($x$) $\Rightarrow$  $A$
\\[0ex]$\Rightarrow$ $\forall$$k$$\in$dom(${\it da}$). $A$=${\it da}$($k$) $\Rightarrow$  $A$
\\[0ex]$\Rightarrow$ $\forall$$x$$\in$dom(${\it ds}$). $A$=${\it ds}$($x$) $\Rightarrow$  AtomFree(Type;$A$)
\\[0ex]$\Rightarrow$ $\forall$$k$$\in$dom(${\it da}$). $A$=${\it da}$($k$) $\Rightarrow$  AtomFree(Type;$A$)
\\[0ex]$\Rightarrow$ \=Feasible(with declarations \+
\\[0ex]ds:${\it ds}$
\\[0ex]da:${\it da}$
\\[0ex]$k$(v) sends $f$ s v on link $l$)
\-
\end{tabbing}